es:ES, x, i:Id, T:Type.
(x, y:T. Dec(x = y  T))
 vartype(i;x)  T
 (e', e:E.
 (e  e' 
 ( loc(e') = i
 ( (x after e') = (x when e)  T
 ( (ev:E. e  ev  & ev  e'  & (x after ev) = (x when ev)  T)) 

latex

Definitions

Trans x,y:T. E(x;y), T, True, strong-subtype(A;B), pred(e), b, first(e), WellFnd{i}(A;x,y.R(x;y)), {T}, SQType(T), (e <loc e'), P  Q, P  Q, (x  l), A & B, P  Q, x. t(x), S  T, (xL.P(x)), [e, e'], False, x:A. B(x), P & Q, A, e  e' , x when e, x:A. B(x), E, P  Q, Id, loc(e), t  T, (x after e), ES, Dec(P), Prop, vartype(i;x)

Lemmas

es-vartype wf, es-after wf, es-loc wf, es-when wf, es-E wf, decidable wf, Id wf, event system wf, es-le wf, not wf, decidable not, es-interval wf2, decidable l exists, member-es-interval, l member subtype, l exists wf, es-locl wf, es-locl-wellfnd, es-le-loc, es-first wf, decidable assert, es-locl-iff, es-axioms, es-pred wf, es-pred-locl, es-loc-pred, l member wf, strong-subtype-self, strong-subtype-set3, strong-subtype-l member, true wf, squash wf, member wf, es-le-trans